Fischer's Mutual Exclusion Example

Fischer's Mutual Exclusion Example

This protocol we examined here is a mutual exclusion protocol, first proposed by Fischer in 1985. Instead of using atomic test-and-set instructions or semaphores, as is often done to assure mutual exclusion nowadays, Fischer's protocol only assumes atomic reads and writes to a shared variable (when the first mutual exclusion protocols were developed in the late 1960s all exclusion protocols were of the "shared variable kind", later on researchers have more concentrated on the "semaphore kind" of protocol). Mutual exclusion in Fischer's Protocol is guaranteed by carefully placing bounds on the execution times of the instructions, leading to a protocol which is very simple, and relies heavily on time aspects.

#define N 4;
#define Delta 3;
#define Epsilon 4;
#define Idle -1;
var x = Idle;
var counter;
P(i) = ifb(x == Idle) {
((update.i{x = i} -> Wait[Epsilon]) within[Delta]);
if (x == i) {
cs.i{counter++} -> exit.i{counter--; x=Idle} -> P(i)
} else {
P(i)
};
FischersProtocol = ||| i:{0..N-1}@P(i);
FischersProtocolDiv = ||| i:{0..N-1}@(P(i) \ {update.i, cs.i, exit.i});
#assert FischersProtocol deadlockfree;
#assert FischersProtocolDiv divergencefree;
#assert FischersProtocolDiv divergencefree<T>;
//mutual exclusion testing
#define MutualExclutsionFail counter > 1;
#assert FischersProtocol reaches MutualExclutsionFail;
//verifying responsiveness by LTL model checking
#define request x != Idle;
#define accessCS counter > 0;
#assert FischersProtocol |= [](request -> <>accessCS);
#assert FischersProtocol |= [](update.0 -> <>cs.0);